1. $A$ : Type
\\[0ex]2. $f$ : $A$$\rightarrow$($A$ + Top)
\\[0ex]3. p{-}inject($A$;$A$;$f$)
\\[0ex]$\vdash$  p{-}inject($A$;$A$;$f$\^{}0)